Section: Partnerships and Cooperations

National initiatives

U3CAT

Participants : Jean-Christophe Filliâtre, Claude Marché [contact] , Guillaume Melquiond, Kalyan Krishnamani, Asma Tafat, Paolo Herms.

U3CAT (Unification of Critical C Code Analysis Techniques) is a project funded by ANR within its programme “Systèmes Embarqués et Grandes Infrastructures - ARPEGE”. It aims at verification techniques of C programs, and is partly a follow-up of the former CAT project. It started in January 2009 and will end in 2012.

The main goal of the project is to integrate various analysis techniques in a single framework, and make them cooperate in a sound way. We address the following general issues:

• Verification techniques for floating-point programs;

• Specification and verification of dynamic or temporal properties;

• Combination of static analysis techniques;

• Management of verification sessions and activities;

• Certification of the tools chains for compilation and for verification.

Partners: CEA-List (Saclay, project leader), Lande team (INRIA Rennes), Gallium team (INRIA Rocquencourt), Dassault Aviation (Saint-Cloud), Airbus France (Toulouse), ATOS Origin (Toulouse), CNAM Cedric laboratory (Evry), CS Communication & Systems (Toulouse), Hispano-Suiza/Safran (Moissy-Cramayel).

INRIA ADT Alt-Ergo

Participants : Sylvain Conchon [contact] , Evelyne Contejean, Claude Marché, Alain Mebsout, Mohamed Iguernelala.

The ADT (Action de Développement Technologique) Alt-Ergo is a 2-years project funded by INRIA, started in September 2009.

The goal is the maturation of the Alt-Ergo prover towards its use in an industrial context in particular for avionics. The expected outcomes of this ADT are the following:

• improving the efficiency of Alt-Ergo;

• fine tuning of Alt-Ergo for the SMT competition;

• generation of counter-examples;

• the qualification of Alt-Ergo for the norm DO-178B.

External Collaborators: Airbus France (Toulouse), Dassault Aviation (Saint-Cloud), team Typical (INRIA, École Polytechnique).

FOST

Participants : Sylvie Boldo [contact] , Jean-Christophe Filliâtre, Guillaume Melquiond.

FOST (Formal prOofs of Scientific compuTation programs) is a 3 years ANR “Blanc” project started in January 2009. S. Boldo is the principal investigator of this project. http://fost.saclay.inria.fr

The FOST project follows CerPAN's footprints as it aims at developing new methods to bound the global error of a numerical program. These methods will be very generic in order to prove a large range of numerical analysis programs. Moreover, FOST aims at providing reusable methods that are understandable by non-specialists of formal methods.

Partners: University Paris 13, INRIA Paris - Rocquencourt (Estime).

SCALP

Participants : Christine Paulin-Mohring [contact] , David Baelde, Xavier Urbain.

This project is funded by ANR (program SESUR). http://scalp.gforge.inria.fr/

It started on january 2008 for 4 years; the coordinator is Yassine Lakhnech from VERIMAG.

The SCALP project (Security of Cryptographic Algorithms with Probabilities) aims at developing automated tools for the verification of cryptographic systems.

Partners: Verimag, INRIA Sophia-Antipolis(Everest then Marelle team), ENS Lyon, LRI, CNAM.

DECERT

Participants : Sylvain Conchon, Évelyne Contejean, Stéphane Lescuyer.

DECERT (DEduction and CERTification) is an ANR “Domaines Emergents” project. It started on January 2009 for 3 years; the coordinator is Thomas Jensen from the Lande team of IRISA/INRIA Rennes.

The goal of the project DECERT is to design and implement new efficient cooperating decision procedures (in particular for fragments of arithmetics), to standardize output interfaces based on certificates proof objects and to integrate SMT provers with skeptical proof assistants and larger verification contexts such as the Rodin tool for B and the Frama-C/Jessie tool chain for verifying C programs.

The partners are: CEA List, LORIA/INRIA Nancy - Grand Est, IRISA/INRIA Rennes - Bretagne Atlantique, INRIA Sophia Antipolis - Méditerranée, Systerel